Nuprl Lemma : R-Dsys-Rall2
0,22
postcript
pdf
L
:Top List,
R
:Top. [[
x
L
.
R
(
x
)]] ~
(map(
x
.[[
R
(
x
)]];
L
))
latex
Definitions
x
:
A
.
B
(
x
)
,
Top
,
[[
R
]]
,
(
L
)
,
map(
f
;
as
)
,
reduce(
f
;
k
;
as
)
,
x
.
t
(
x
)
,
t
T
,
Y
,
x
(
s
)
Lemmas
Rall-nil
,
Rall-cons
,
top
wf
origin
L:Top List, R:Top. [[
x
L.R(x)]] ~ (map(
x.[[R(x)]];L)) L:Top List, R:Top. [[xL.R(x)]] ~ (map(x.[[R(x)]];L)) x:A. B(x)(L)
x. t(x) T